Reffect(${\it loc}$; ${\it ds}$; ${\it knd}$; $T$; $x$; $f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$inr inr inr inr inr (inl $<$${\it loc}$, ${\it ds}$, ${\it knd}$, $T$, $x$, $f$$>$ )